Nuprl Lemma : s-insert_wf
0,22
postcript
pdf
T
:Type.
T
(
x
:
T
,
L
:
T
List. s-insert(
x
;
L
)
T
List)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
i
<
j
,
if
b
t
else
f
fi
,
i
=
j
,
s-insert(
x
;
l
)
,
P
Q
Lemmas
eq
int
wf
,
ifthenelse
wf
,
lt
int
wf
origin
T:Type. T 
(x:T, L:T List. s-insert(x;L) 
T List) T:Type. T (x:T, L:T List. s-insert(x;L) T List) Tx:A. B(x)
j
t else f fij Q